Calculus of Constructions
#Fleeting_Notes
Calculus of Constructions(CoC)
端的に表しすぎると下記で構成されるはず
単純型付きラムダ計算 + 依存型 + 型構築子 + ポリモーフィズム(多相型)
ラムダ・キューブでは、単純型付きラムダ計算からCoCにどうやって至るか(?)が表されている
λCがCoC
CoCに帰納型を加えるとCalculus of Inductive Constructions(CIC)になる
確認用
Q. Calculus of Constructions
関連
『The Calculus of Constructions』
Thierry Coquand and G ́erard Huet. The Calculus of Constructions. PhD thesis, INRIA, 1986.
メモ
ラムダ計算と Calculus of Constructions の定義解説 | Mathlog
調査用
Google.icon Calculus of Constructions(日)
Google.icon Calculus of constructions(英)
Wikipedia.icon
Calculus of Constructions - Wikipedia(日)
Calculus of Constructions(検索) - Wikipedia(日)
Wikipedia.icon
Calculus of constructions - Wikipedia(英)
Calculus of constructions(検索) - Wikipedia(英)
#λC